ES(the_w)
== <E
== , product-deq(Id;;IdDeq;NatDeq)
== , e.w-pred(the_w;e)
== , e.w-info(the_w;e)
== , TERMOF{w-order-axioms:ObjectId, 1:l, i:l}(the_w,p)
== , the_w.T
== , the_w.TA
== , the_w.M
== , i,x. s(i;0).x
== , i.(w-machine(the_w;i).2).1
== , e.val(e)
== , i.w-machine(the_w;i).2.2
== , i.w-machine(the_w;i).1
== , e.time(e)
== , TERMOF{world-es-val:ObjectId, 1:l, i:l}(the_w,p)
== , TERMOF{w-causl-time2:ObjectId, 1:l, i:l}(the_w,p)
== , i,x. discrete(i;x)
== , TERMOF{world-es-const:ObjectId, 1:l, i:l}(the_w,p)
== , > 

latex

---

clarification:

w-es{i:l}
w-es(the_w; p)
== <w-E(the_w)
== , product-deq(Id;;IdDeq;NatDeq)
== , e.w-pred(the_w;e)
== , e.w-info(the_w;e)
== , TERMOF{w-order-axioms:ObjectId, 1:l, i:l}(the_w,p)
== , the_w.T
== , the_w.TA
== , the_w.M
== , i,x. w-s(the_w; i; 0; x)
== , i.(w-machine(the_w;i).2).1
== , e.w-eval(the_w; e)
== , i.w-machine(the_w;i).2.2
== , i.w-machine(the_w;i).1
== , e.w-time(the_w; e)
== , TERMOF{world-es-val:ObjectId, 1:l, i:l}(the_w,p)
== , TERMOF{w-causl-time2:ObjectId, 1:l, i:l}(the_w,p)
== , i,x. w-discrete(the_w;i;x)
== , TERMOF{world-es-const:ObjectId, 1:l, i:l}(the_w,p)
== , > 

latex

Definitions	E, product-deq(A;B;a;b), Id, , IdDeq, NatDeq, w-pred(w;e), w-info(w;e), w-order-axioms, w.T, w.TA, w.M, s(i;t).x, #$n, val(e), t.2, t.1, w-machine(w;i), time(e), world-es-val, w-causl-time2, x.A(x), discrete(i;x), <a, b>, f(a), world-es-const,
FDL editor aliases	w-es